To be able to verify the correctness of computer systems, no matter whether they are hardware, software or a combination, is of great importance. Well, there are essential problems which cannot be discovered by current techniques. For instance, the concurrent bugs are among the most difficult to be found by testing, since they tend to be non-reproducible or not covered by test cases [HUTH&Ryan04]. Thus it is well worth having handy verification tools to simulate the system behaviors and verify critical properties such as safety, concurrency, liveness and fairness. Then comes our Process Analysis Toolkit (PAT)!

What is PAT?

Process Analysis Toolkit (also known as PAT, available at http://www.patroot.com) is designed to apply state-of-the-art model checking techniques for system analysis.

At first we developed this tool to investigate system (specified using the classic process algebra Communicating Sequential Processes - CSP) verification under fairness assumptions. The motivation is that fairness assumptions are often necessary in system verification practice in order to prove desirable system properties, whereas existing languages and tools have limited support for fairness modeling as well as verification. Since then, PAT has been evolved to be a self-contained framework to support reach-ability analysis, deadlock-freeness analysis, full LTL (linear temporal logic) model checking, refinement checking as well as a powerful simulator. It is a user-friendly model checker for all users.

Starting from PAT 2.0, we applied a modularized design to support the analysis of the different system/languages. Each language is encapsulated as one module with predefined APIs, which identify the (specialized) language syntax, well-formed rules as well as (operational) formal semantics, and loaded at run time according to the input model. This layered architecture allows new languages to be developed easily by providing the syntax rules and semantics. Till now, eleven modules have been developed, namely Communicating Sequential Processes (CSP) module, Web Service (WS) module, Real-Time System Module, Probability CSP Module, Orc Module, Security Module and NesC Module etc.. In the future, our targeted systems include C# program and UML (state chart and sequence diagrams) and so on. Please refer to Chapter 3 the Process Analysis Toolkit for detailed information.

From PAT 3.0, we emphysis the extension and creating custimized model checkers, which provides the different interfaces for domain experts to create their model checkers with minimum efforts. There are several ways to create your dedicated model checker which will be introduced in section 5.3 PAT extensions. You can create a new module either by easy translation or extending the languange syntax or apply new properties and corresponding checking algorithms or building a completely new module following the steps and using pre-defined API as we will show you.